f31ba263bb22a944bba521605b375d5d8b76fdbb,org.coreasm.engine/src/org/coreasm/engine/plugins/predicatelogic/PredicateLogicPlugin.java,PredicateLogicPlugin,interpretExists,#Interpreter#ASTNode#,385
Before Change
if (s == null) {
Enumerable domain = (Enumerable)variable.getValue().getValue();
if (domain.supportsIndexedView())
s = new ArrayList<Element>(domain.getIndexedView());
else
s = new ArrayList<Element>(((Enumerable) variable.getValue().getValue()).enumerate());
if (s.isEmpty()) {
for (Entry<String, ASTNode> var : variableMap.entrySet()) {
if (remained.remove(var.getValue()) != null)
interpreter.removeEnv(var.getKey());
}
// [pos] := (undef,undef,ff)
existsExpNode.setNode(null, null, BooleanElement.FALSE);
return existsExpNode;
}
remained.put(variable.getValue(), s);
shouldChoose = true;
}
else if (shouldChoose)
interpreter.removeEnv(variable.getKey());
if (shouldChoose) {
if (!s.isEmpty()) {
// SPEC: considered := considered union {t}
// choose t in s, for simplicty choose the first
// since we have to go through all of them
Element chosen = s.remove(0);
shouldChoose = false;
// SPEC: AddEnv(x,t)
After Change
if (it == null) {
Enumerable domain = (Enumerable)variable.getValue().getValue();
if (domain.supportsIndexedView())
it = domain.getIndexedView().iterator();
else
it = domain.enumerate().iterator();
if (!it.hasNext()) {
for (Entry<String, ASTNode> var : variableMap.entrySet()) {
if (iterators.remove(var.getValue()) != null)
interpreter.removeEnv(var.getKey());
}
// [pos] := (undef,undef,ff)
existsExpNode.setNode(null, null, BooleanElement.FALSE);
return existsExpNode;
}
iterators.put(variable.getValue(), it);
shouldChoose = true;
}
else if (shouldChoose)
interpreter.removeEnv(variable.getKey());
if (shouldChoose) {
if (it.hasNext()) {
// SPEC: considered := considered union {t}
Element chosen = it.next();
shouldChoose = false;
// SPEC: AddEnv(x,t)